IsAction(A;x;e;S;f) == (
a, b:A, u:S. ((a x b) f u) = (a f (b f u))) & (u:S. (e f u) = u)
clarification:
basic
IsAction(A;x;e;S;f)
== (
a:A, b:A, u:S. ((a x b) f u) = (a f (b f u)) 
S) & (u:S. (e f u) = u S) | 13,42 |
a, b:A, u:S. ((a x b) f u) = (a f (b f u))) & (u:S. (e f u) = u)
a:A, b:A, u:S. ((a x b) f u) = (a f (b f u)) S) & (u:S. (e f u) = u S)
| Up | |
| Wellformedness Lemmas | |
| Definitions | x:A. B(x) |